$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$$B$). Bij($A$;$B$;$f$) $\Rightarrow$ ($\exists$$g$:$B$$\rightarrow$$A$. InvFuns($A$;$B$;$f$;$g$))